package plus;

public class Type {
	Type mergeTarget;
	private Solution solution; // invariant: present if neither free nor merged.
	public Type chase() {
		if (mergeTarget == null) return this;
		if (mergeTarget == this) throw null;
		mergeTarget = mergeTarget.chase();
		return mergeTarget;
	}
	boolean isFree() {return solution==null;}
	boolean isNil() {return kind()==S_Nil.class;}
	Class<? extends Solution> kind() { return isFree() ? null : solution.getClass(); }
	public static Type unify(Type a, Type b) {
		if (null == b) return a.chase();
		a=a.chase();
		b=b.chase();
		if (a == b) return a;
		Uni.progress = true;
		if (a.isFree()) { a.point_to(b); return b; }
		else if (b.isFree() || a.solution == b.solution) { b.point_to(a); return a; }
		else if (a.kind() == b.kind()) return merge(a,b);
		else if (a.kind() == S_Nil.class && b.solution.isNullable() ) {
			a.mergeTarget = b;
			a.solution = null;
			return b;
		} else if (a.solution.isNullable() && b.kind() == S_Nil.class ) {
			b.mergeTarget = a;
			b.solution = null;
			return a;
		} else {
			// TODO Eventually figure out how to make it more general and allow
			// TODO for variant records
			mismatch(a.toString(), b.toString());
			throw null;
		}
	}
	private static Type merge(Type a, Type b) {
		b.mergeTarget = a;
		a.solution.unify_with(b.solution);
		b.solution = null; // hint to the garbage collector...
		return a;
	}
	private void point_to(Type that) { Uni.progress = true; mergeTarget = that; }
	static void unify(Type[] a, Type[] b) { for (int i=0; i<a.length; i++) a[i] = unify(a[i], b[i]); }
	public static void mismatch(String msg) { throw new Gripe("Type mismatch: "+msg+"."); }
	public static void mismatch(String a, String b) { mismatch(a+" vs "+b); }
	public void conform_to(Type that, Gamma gamma) {
		if (mergeTarget != null) {
			chase().conform_to(that, gamma);
			return;
		}
		that = that.chase();
		if (that.isFree()) gamma.assign(this, that);
		else if (this.isFree()) {
			// Instantiate a blank copy of "that":
			Uni.progress = true;
			solution = that.solution.copy();
			solution.conform_to(that.solution, gamma);
		} else if (this.kind() == that.kind()) solution.conform_to(that.solution, gamma);
		else if (this.kind() == S_Nil.class && that.solution.isNullable()) {
			// adopt implied record type:
			Uni.progress = true;
			solution = that.solution.copy();
		}
		else mismatch(this.kind()+" is no match for "+that.kind());
	}
	static void conform(Type[] as, Type[] bs, Gamma g) {
		int i=as.length;
		while (i-->0) { 
			as[i].conform_to(bs[i], g);
			as[i] = as[i].chase();
		}
	}
	static boolean canConform(Type near, Type far, Hypo h) {
		assert near != null;
		assert far != null;
		assert h != null;
		near = h.rep(near); far = h.rep(far);
		if (near == far) return true;
		else if (near.isFree()) h.assume(near, far);
		else if (far.isFree()) h.assume(far, near);
		else if (near.kind() == far.kind()) return near.solution.canConform(far.solution, h);
		else if (near.kind() == S_Nil.class && far.solution.isNullable()) {
			h.assume(near, far);
		} else if (far.kind() == S_Nil.class && near.solution.isNullable()) {
			h.assume(far, near);
		}
		else return false;
		return true;
	}
	public static boolean canConform(Type[] as, Type[] bs, Hypo h) {
		int i=as.length;
		while (i-->0) if (!canConform(as[i], bs[i], h)) return false;
		return true;
	}
	public static Type[] fresh_vars(int nr) {
		Type[] vars = new Type[nr];
		while (nr-->0) vars[nr] = new Type();
		return vars;
	}
	public static Type variable() { return new Type(); }
	public static Type fresh(Solution s) {
		Type t = new Type();
		t.solution = s;
		return t;
	}
	public void unify_with(Solution s) {
		if (mergeTarget != null) chase().unify_with(s);
		else if (isFree()) { solution = s; Uni.progress = true; }
		else if (kind() == s.getClass()) solution.unify_with(s);
		else mismatch(toString(), s.toString());
	}
	public String toString() { Type a = chase(); return a.isFree() ? "?" : a.solution.toString(); }
	public static Type[] subst(Type[] params, Type[] actuals) {
		Type[] result = new Type[params.length];
		for (int i=0; i<result.length; i++) {
			result[i] = params[i].chase().subst(actuals);
		} 
		return result;
	}
	Type subst(Type[] actuals) {
		return isFree() ? this : solution.subst(actuals); 
	}
	public boolean unifyField(String field, Type that, int lineNr) {
		if (isFree()||isNil()) return false; // no effect
		else if (kind() == S_Record.class) {
			S_Record sol = (S_Record)solution;
			unify(sol.typeOfField(field), that);
			return true;
		} else throw new Gripe("Cannot access field "+field+": value is not a record.");
	}
	public Solution getSolution() { return chase().solution; }
}
